;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "mmirroring.lisp")
(require "mbmptree.lisp")
(require "mdatagenerators.lisp")

(module Tmirroring
  (import Imirroring)
  (import Ibmptree)
  (import IDataGenerators)
  
  (include-book "testing" :dir :teachpacks)
  (include-book "doublecheck" :dir :teachpacks)
  
  ; Generates a random pixel (random RGB values).
  (defrandom random-pixel ()
    (let* ((r (random-between 0 255))
           (g (random-between 0 255))
           (b (random-between 0 255)))
      (list r g b)))
  
  ; Random bitmap file, uses a static header with a 
  ; size of heightxwidth.
  (defrandom random-bitmap (height width)
    (let* ((header (list 66 77 54 12 0 0 0 0 0 0 54 0 0 
                         0 40 0 0 0 width 0 0 0 height 0 0 0 1 
                         0 24 0 0 0 0 0 0 12 0 0 0 0 0 
                         0 0 0 0 0 0 0 0 0 0 0 0 0))
           (pixels (random-list-of (random-pixel) :size (* width height)))
           (tr (insert-header (empty-bmp-tree) header)))
      (fill-bitmap tr 0 0 height width pixels)))
  
  ; Tests a legal vertical mirror case
  (check-expect (mirror (make-bmp-tree 
                         (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                      0 0 0 0 0 0 3 0 0 0 3)
                               (list 0 0 (list 1 1 1)) 
                               (list 0 1 (list 2 2 2))
                               (list 0 2 (list 3 3 3)) 
                               (list 1 0 (list 4 4 4))
                               (list 1 1 (list 5 5 5)) 
                               (list 1 2 (list 0 0 0))
                               (list 2 0 (list 7 7 7)) 
                               (list 2 1 (list 8 8 8))
                               (list 2 2 (list 9 9 9))))
                        "vertical")
                (make-bmp-tree 
                 (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                             0 0 0 0 0 0 3 0 0 0 3)
                       (list 0 0 (list 7 7 7)) 
                       (list 0 1 (list 8 8 8))
                       (list 0 2 (list 9 9 9)) 
                       (list 1 0 (list 4 4 4))
                       (list 1 1 (list 5 5 5)) 
                       (list 1 2 (list 0 0 0))
                       (list 2 0 (list 1 1 1)) 
                       (list 2 1 (list 2 2 2))
                       (list 2 2 (list 3 3 3)))))
  
  ; Tests a legal horizontal mirror case
  (check-expect (mirror (make-bmp-tree 
                         (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                      0 0 0 0 0 0 3 0 0 0 3)
                               (list 0 0 (list 1 1 1)) 
                               (list 0 1 (list 2 2 2))
                               (list 0 2 (list 3 3 3)) 
                               (list 1 0 (list 4 4 4))
                               (list 1 1 (list 5 5 5)) 
                               (list 1 2 (list 0 0 0))
                               (list 2 0 (list 7 7 7)) 
                               (list 2 1 (list 8 8 8))
                               (list 2 2 (list 9 9 9))))
                        "horizontal")
                (make-bmp-tree 
                 (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                             0 0 0 0 0 0 3 0 0 0 3)
                       (list 0 0 (list 3 3 3)) 
                       (list 0 1 (list 2 2 2))
                       (list 0 2 (list 1 1 1)) 
                       (list 1 0 (list 0 0 0))
                       (list 1 1 (list 5 5 5)) 
                       (list 1 2 (list 4 4 4))
                       (list 2 0 (list 9 9 9)) 
                       (list 2 1 (list 8 8 8))
                       (list 2 2 (list 7 7 7)))))
  
  ; Tests nil cases for vertical and horizontal orientations
  (check-expect (mirror nil "vertical") nil)
  (check-expect (mirror nil "horizontal") nil)
  
  ; Tests a case with an illegal orientation
  (check-expect (mirror (make-bmp-tree 
                         (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                                     0 0 0 0 0 0 3 0 0 0 3)
                               (list 0 0 (list 1 1 1)) 
                               (list 0 1 (list 2 2 2))
                               (list 0 2 (list 3 3 3)) 
                               (list 1 0 (list 4 4 4))
                               (list 1 1 (list 5 5 5)) 
                               (list 1 2 (list 0 0 0))
                               (list 2 0 (list 7 7 7)) 
                               (list 2 1 (list 8 8 8))
                               (list 2 2 (list 9 9 9))))
                        "durp")
                (make-bmp-tree 
                 (list (list 0 0 0 0 0 0 0 0 0 0 0 0
                             0 0 0 0 0 0 3 0 0 0 3)
                       (list 0 0 (list 1 1 1)) 
                       (list 0 1 (list 2 2 2))
                       (list 0 2 (list 3 3 3)) 
                       (list 1 0 (list 4 4 4))
                       (list 1 1 (list 5 5 5)) 
                       (list 1 2 (list 0 0 0))
                       (list 2 0 (list 7 7 7)) 
                       (list 2 1 (list 8 8 8))
                       (list 2 2 (list 9 9 9)))))

  ; Verifies that mirror always mirroring vertically always
  ; returns a true bmp-tree
  (defproperty mirror-vertical-returns-true-bmp-tree-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     bitmap :value (random-bitmap height width))
    (true-bmp-tree? (mirror bitmap "vertical")))
  
  ; Verifies that mirror always mirroring horizontally always
  ; returns a true bmp-tree
  (defproperty mirror-horizontal-returns-true-bmp-tree-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     bitmap :value (random-bitmap height width))
    (true-bmp-tree? (mirror bitmap "horizontal")))

  ; Verifies that mirror works with vertical orientation by
  ; showing that each original row is moved to its correct
  ; position in the vertically flipped image
  (defproperty mirror-vertical-works-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     row :value (random-between 0 (- height 1))
     bitmap :value (random-bitmap height width))
    (equal (get-row bitmap row)
           (get-row (mirror bitmap "vertical") 
                    (- (- height row) 1))))

  ; Verifies that mirror works with horizontal orientation by
  ; showing that each original pixel is moved to its correct
  ; position in the horizontally flipped image
  (defproperty mirror-horizontal-works-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     row :value (random-between 0 (- height 1))
     column :value (random-between 0 (- width 1))
     bitmap :value (random-bitmap height width))
    (equal (get-pixel-color bitmap row column)
           (get-pixel-color (mirror bitmap "horizontal") 
                            row (- (- width column) 1))))

  ; Verifies that mirroring vertical twice returns the 
  ; original bitmap
  (defproperty mirror-vertical-round-trip-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     bitmap :value (random-bitmap height width))
    (equal bitmap
           (mirror (mirror bitmap "vertical") "vertical")))  

  ; Verifies that mirroring horizontal twice returns the 
  ; original bitmap
  (defproperty mirror-horizontal-round-trip-prp
    (height :value (random-between 1 25)
     width :value (random-between 1 25)
     bitmap :value (random-bitmap height width))
    (equal bitmap
           (mirror (mirror bitmap "horizontal") "horizontal")))  
  )

(link RTmirroring (Mavltree Mbmptree Mdatagenerators 
                            Mmirroring Tmirroring))
(invoke RTmirroring)